/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package chameleon.model.formula.parser;

import chameleon.model.formula.Operator;
import chameleon.model.formula.Tag;
import java.io.IOException;

/** This class is a parser for a boolean formula which accepts operator :
 * ->, || , &&, <->, next, !, ~, =, FALSE, TRUE
 *
 * The syntax is the following
 *
 * f :: TRUE | FALSE | {!,~, next} f | {->, <->, &, |, =} f | (f) |
 *
 * @author simon
 */
public class BooleanParser extends AbstractParser {

    public BooleanParser (String input) {
        super();
        lineRead = input;
    }

    /**
     * return the nex token.
     * @return
     * @throws IOException
     */

    @Override
    protected Word nextToken() throws IOException{

        String prop ="";
        char[] line = lineRead.toCharArray();
        char charRead;
        boolean haveProp = false;
        while (lineRead !=null ){

            if (pos_ == line.length){
                if (haveProp){
                    haveProp = false;
                    return new Word (prop,Tag.PROPOSITION);
                }
                /*if((lineRead = br.readLine()) != null){
                    line = lineRead.toCharArray();
                    pos_ = 0;
                */
                else
                    return new Word (Tag.S_END,Tag.END);
            }

            charRead = line[pos_];
            pos_++;

            if (charRead == '!' && line[pos_] == '='){
                if (!haveProp){
                    pos_++;
                    return new Word(Tag.S_NOTEQUAL,Tag.NOTEQUAL);
                }
                else{
                    pos_--;
                    return new Word(prop,Tag.PROPOSITION);
                }
            }
            else if(charRead == '!' || charRead == '~'){
                if (!haveProp)
                    return new Word (Tag.S_NOT,Tag.NOT);
                else{
                    pos_--;
                    return new Word(prop,Tag.PROPOSITION);
                }
            }
            else if (charRead == '('){
                return new Word(Tag.S_OPEN_PARENTHESE,Tag.OPEN_PARENTHESE);
            }
            else if (charRead == '=' && line[pos_] == '='){
                if (!haveProp){
                    pos_++;
                    return new Word(Tag.S_EQUAL,Tag.EQUAL);
                }
                else{
                    pos_--;
                    return new Word(prop,Tag.PROPOSITION);
                }
            }
            else if (charRead == '='){
                if (!haveProp)
                    return new Word(Tag.S_ASSIGN,Tag.ASSIGN);
                else{
                    pos_--;
                    return new Word(prop,Tag.PROPOSITION);
                }
            }

            else if (charRead == ')'){
                if (!haveProp)
                    return new Word(Tag.S_CLOSE_PARENTHESE,Tag.CLOSE_PARENTHESE);
                else{
                    pos_--;
                    return new Word(prop,Tag.PROPOSITION);
                }
            }
            else if (charRead == '&' && line[pos_] == '&' ){
                if (!haveProp){
                    pos_++;
                    return new Word(Tag.S_AND, Tag.AND);
                }
                else{
                    pos_--;
                    return new Word(prop,Tag.PROPOSITION);
                }
            }
            else if (charRead == '|' && line[pos_] == '|' ){
                if (!haveProp){
                    pos_++;
                    return new Word(Tag.S_OR,Tag.OR);
                }
                else{
                    pos_--;
                    return new Word(prop,Tag.PROPOSITION);
                }
            }            
            else if (charRead == '<' && line[pos_]=='='){
                if (!haveProp){
                    pos_++;
                    return new Word(Tag.S_LE,Tag.LE);
                }
                else{
                    pos_--;
                    return new Word(prop,Tag.PROPOSITION);
                }
            }
            else if (charRead == '<' ){
                if (!haveProp){
                    return new Word(Tag.S_LT,Tag.LT);
                }
                else{
                    pos_--;
                    return new Word(prop,Tag.PROPOSITION);
                }
            }          
            else if (charRead == '>' && line[pos_]=='='){
                if (!haveProp){
                    pos_++;
                    return new Word(Tag.S_GE,Tag.GE);
                }
                else{
                    pos_--;
                    return new Word(prop,Tag.PROPOSITION);
                }
            }
            else if (charRead == '>' ){
                if (!haveProp){
                    return new Word(Tag.S_GT,Tag.GT);
                }
                else{
                    pos_--;
                    return new Word(prop,Tag.PROPOSITION);
                }
            }
            else if (charRead == '-' && line[pos_] == '>'){
                if (!haveProp){
                    pos_++;
                    return new Word(Tag.S_IMPLIES,Tag.IMPLIES);
                }
                else{
                    pos_--;
                    return new Word(prop,Tag.PROPOSITION);
                }
            }
            else if (charRead == '<' && line[pos_] == '-' && line[pos_+1] == '>'){
                if (!haveProp){
                    pos_ += 2;
                    return new Word(Tag.S_EQUIVALENCE,Tag.EQUIVALENCE);
                }
                else{
                    pos_--;
                    return new Word(prop,Tag.PROPOSITION);
                }
            }
            else if (isLessThanMax(3) && charRead == 'n' && line[pos_] == 'e' && line[pos_+1] == 'x'
                    && line[pos_+2] == 't'){
                pos_ += 2;
                if (!haveProp)
                    return new Word(Tag.S_NEXT_TRANSITION,Tag.NEXT_TRANSITION);
                else{
                    pos_--;
                    return new Word(prop,Tag.PROPOSITION);
                }
            }
            else if (isLessThanMax(3) && charRead == 'T' && line[pos_] == 'R' && line[pos_+1] == 'U'
                    && line[pos_+2]=='E'){
                pos_ += 3;
                return new Word(Tag.S_TRUE,Tag.TRUE);
            }
            else if (isLessThanMax(4) &&charRead == 'F' && line[pos_] == 'A' && line[pos_+1] == 'L'
                    && line[pos_+2]=='S' && line[pos_+3] == 'E'){
                pos_ += 4;
                return new Word(Tag.S_FALSE,Tag.FALSE);
            }
            else if (Character.isWhitespace(charRead)){
                if (haveProp)
                    return new Word (prop,Tag.PROPOSITION);
            }
            /*else if (charRead == '\n'){
                lineRead = br.readLine();
            }*/
            else{
                //We have a proposition
                prop += charRead;
                haveProp = true;
            }
        }
        if (haveProp)
            return new Word(prop, Tag.PROPOSITION);
        return new Word(Tag.S_END,Tag.END);
    }

    /**
     * This method push on the corresponding stack the token elemnt.
     *
     * If isOp == true we have an operator, otherwise we have a formula.
     *
     * If we have a formula, we create first a mathemtical expression before push.
     *
     * @param isOp
     * @throws IOException
     */

    @Override
    protected void push(boolean isOp) throws IOException{
        
        if (isOp)
            stackOperator_.push(new Operator(token_.toString()));
        else{
            MathematicalParser parser = new MathematicalParser(token_.toString());
            stackFormula_.push(parser.createFormula());
        }
        token_ = nextToken();
    }

    //START OF PARSING

    /**
     * The following methods are the description of the grammar.
     */

    protected void FORMULA() throws IOException{
        NOTEQUAL();
    }

    private void NOTEQUAL() throws IOException{
        EQ();
        NOTEQUALP();
    }

    private void NOTEQUALP() throws IOException{
        if (match(Tag.NOTEQUAL) || match(Tag.EQUAL)){
            push(true);
            EQ();
            NOTEQUALP();
            createFormulaOnStack();
        }
        else
            ;//End of recursion
    }

    private void EQ() throws IOException{
        IMPLIES();
        EQUIVALENCE();
    }

    private void EQUIVALENCE() throws IOException{
        if (match(Tag.EQUIVALENCE)){
            push(true);
            IMPLIES();
            EQUIVALENCE();
            createFormulaOnStack();
        }
        else
            ;//End of recursion
    }

    private void IMPLIES() throws IOException{
        OR();
        IMPLIESP();
    }

    private void IMPLIESP() throws IOException{
        if (match(Tag.IMPLIES)){
            push(true);
            OR();
            IMPLIESP();
            createFormulaOnStack();
        }
    }

    private void OR() throws IOException {
        AND();
        ORP();
    }

    private void ORP() throws IOException{
        if (match(Tag.OR)){
            push(true);
            AND();
            ORP();
            createFormulaOnStack();
        }
        else
            ;//End of recursion
    }

    private void AND() throws IOException{
        ASSIGN();
        ANDP();
    }

    private void ANDP() throws IOException {
        if (match(Tag.AND)){
            push(true);
            ASSIGN();
            ANDP();
            createFormulaOnStack();
        }
        else
            ;//End of recursion
    }

    private void ASSIGN() throws IOException{
        INEQUALITYOP();
        ASSIGNP();
    }

    private void ASSIGNP() throws IOException{
        if (match(Tag.ASSIGN)){
            push(true);
            INEQUALITYOP();
            ASSIGNP();
            createFormulaOnStack();
        }
        else
            ;//End of recursion
    }

    private void INEQUALITYOP() throws IOException{
        NEXT();
        INEQUALITYOPP();
    }
    
    private void INEQUALITYOPP() throws IOException{
        if (match(Tag.LT) || match(Tag.LE) || match(Tag.GT) || match(Tag.GE)){
            push(true);
            NEXT();
            INEQUALITYOPP();
            createFormulaOnStack();
        }
        else
            ;//end of recursion
    }
    
    private void NEXT() throws IOException {
        if (match(Tag.NEXT_TRANSITION)){
            push(true);
            FORMULA();
            createFormulaOnStack();
        }
        else
            NOT();
    }

    private void NOT() throws IOException {
        if (match(Tag.NOT)){
            push(true);
            if (match(Tag.OPEN_PARENTHESE)|| match(Tag.CLOSE_PARENTHESE) ||
                    match(Tag.PROPOSITION) || match (Tag.FALSE) || match (Tag.TRUE))
                FACTOR();
            else
                FORMULA();
            createFormulaOnStack();
        }
        else
            FACTOR();
    }

    private void FACTOR() throws IOException {
        if (match(Tag.OPEN_PARENTHESE)){
            token_ = nextToken();
            FORMULA();
            if (!match(Tag.CLOSE_PARENTHESE))
                throw new IOException("Missing closed parenthese");
            createFormulaOnStack();
            token_ = nextToken();
        }
        else if (match(Tag.PROPOSITION)){
            push(false);
        }
        else if (match(Tag.TRUE)){
            push(false);
        }
        else if (match(Tag.FALSE)){
            push(false);
        }
        else
            throw new IOException("Parse error");
    }

}
